$\forall$$B$:Type, $P$:($B$$\rightarrow\mathbb{B}$). finite{-}type($B$) $\Rightarrow$ finite{-}type(\{$b$:$B$$\mid$ $\uparrow$$P$($b$)\} )